package cz.cvut.fit.mi_paa.sat.strategy;

import cz.cvut.fit.mi_paa.abs.Context;
import cz.cvut.fit.mi_paa.knapsack.Item;
import cz.cvut.fit.mi_paa.sat.SatInstance;

import java.io.FileWriter;
import java.io.IOException;

/**
 * Created with IntelliJ IDEA.
 * User: milos
 * Date: 1.4.13
 * Time: 23:54
 * To change this template use File | Settings | File Templates.
 */
public class BruteForceSatStrategy extends SatStrategy {

    private SatInstance instance;
    private int maxWeight;
    private long iterations;
    private boolean[] best;

    public BruteForceSatStrategy(Context context) {
        super(context);
        instance = (SatInstance) context.getInstance();
        this.iterations = (long) Math.pow(2, instance.getVariableNum());
        best = new boolean[instance.getVariableNum()];
    }

    @Override
    public void solve() throws IOException, CloneNotSupportedException {
        for(long i = 0; i< iterations;i++) {
            boolean[] configuration = getBinaryConfiguration(i);
            if(isSolution(configuration)) {
                if(getWeightSum(configuration) > maxWeight) {
                    maxWeight = getWeightSum(configuration);
                    System.arraycopy(configuration,0,best,0,best.length);
                }
            }
        }
    }

    private boolean[] getBinaryConfiguration(long number) {
        boolean[] binaryArray = new boolean[instance.getVariableNum()];
        for (int j = 0 ; j<instance.getVariableNum() ;j++)   {
            number = (number << 1);
            binaryArray[j] = (((number & iterations) >> instance.getVariableNum()) == 1);
        }
        return binaryArray;
    }

    @Override
    public void writeResult() throws IOException {
        FileWriter resultWriter = context.getResultWriter();
        resultWriter.write("s "+ maxWeight + " ");
        for (boolean b : best) {
            resultWriter.write((b) ? "1" : "0");
        }
        resultWriter.write("\n");

    }
}
